Problem:
 half(0()) -> 0()
 half(s(s(x))) -> s(half(x))
 log(s(0())) -> 0()
 log(s(s(x))) -> s(log(s(half(x))))

Proof:
 Complexity Transformation Processor:
  strict:
   half(0()) -> 0()
   half(s(s(x))) -> s(half(x))
   log(s(0())) -> 0()
   log(s(s(x))) -> s(log(s(half(x))))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [log](x0) = x0 + 43,
     
     [s](x0) = x0 + 21,
     
     [half](x0) = x0 + 48,
     
     [0] = 64
    orientation:
     half(0()) = 112 >= 64 = 0()
     
     half(s(s(x))) = x + 90 >= x + 69 = s(half(x))
     
     log(s(0())) = 128 >= 64 = 0()
     
     log(s(s(x))) = x + 85 >= x + 133 = s(log(s(half(x))))
    problem:
     strict:
      log(s(s(x))) -> s(log(s(half(x))))
     weak:
      half(0()) -> 0()
      half(s(s(x))) -> s(half(x))
      log(s(0())) -> 0()
    Arctic Interpretation Processor:
     dimension: 2
     interpretation:
                  [1  -&]  
      [log](x0) = [2  0 ]x0,
      
                [0 1]  
      [s](x0) = [7 0]x0,
      
                   [0  -&]  
      [half](x0) = [0  -&]x0,
      
            [0 ]
      [0] = [-&]
     orientation:
                     [9  2 ]     [8  -&]                      
      log(s(s(x))) = [10 8 ]x >= [9  -&]x = s(log(s(half(x))))
      
                  [0]    [0 ]      
      half(0()) = [0] >= [-&] = 0()
      
                      [8 1]     [1  -&]              
      half(s(s(x))) = [8 1]x >= [7  -&]x = s(half(x))
      
                    [1]    [0 ]      
      log(s(0())) = [7] >= [-&] = 0()
     problem:
      strict:
       
      weak:
       log(s(s(x))) -> s(log(s(half(x))))
       half(0()) -> 0()
       half(s(s(x))) -> s(half(x))
       log(s(0())) -> 0()
     Qed